/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.ast;

import java.util.Map;

/**
 * Represents an Alloy command that runs an analysis for particular scopes,
 * such as "run ShowExampleExecution for 3 Train, 2 Track" or "check SafetyInvariantPreserved for 4".
 * Both "run" and "check" commands are represented by {@link FindCommand}, which I think is the only
 * kind of {@link Command} implemented right now.
 */
public abstract class Command extends TreeNode {

    /**
     * index of scope in child list
     */
    private static final int SCOPE_INDEX = 0;

    /**
     * Holds the basic information about a Command.  Almost immutable, except for the toString value,
     * which is not known at the time the Command is constructed.  Every time the Command is asked for its info, 
     * it will update the info.toString value.
     * 
     * The purpose of this class is to reduce memory leaks.  Many clients do not actually need the Command object,
     * but just what's in this Info object.  Holding onto the real Command object holds onto the entire AST.
     * @author drayside
     *
     */
    public static class Info {

    	/**
	     * name of the command.  this should probably
	     * be a child, but i'm too lazy to make all the necessary
	     * changes right now.
	     */
	    public final String name;
	    private String toString = "";
	    private boolean hasExpects = false;
	    private int expectsCount = 0;
	    
	    private final int type;
	    private final static int UNKNOWN_TYPE = 0;
	    private final static int CHECK_TYPE = 1;
	    private final static int RUN_TYPE = 2;
	    
    	private Info(final String name, final Command cmd) {
    		this.name = name;

    		if (cmd instanceof CheckCommand) {
    			type = CHECK_TYPE;
    		} else if (cmd instanceof RunCommand) {
    			type = RUN_TYPE;
    		} else {
    			type = UNKNOWN_TYPE;
    		}
    	}

    	/** 
    	 * Used only to construct the EMPTY_COMMAND_INFO.
    	 *
    	 */
    	private Info() {
    		this.name = null;
    		this.type = UNKNOWN_TYPE;
    	}
    	/**
    	 * Used only by NullAnalysis.
    	 */
    	public final static Info EMPTY_COMMAND_INFO = new Info();
    	

    	public boolean isFindCommand() {
    		return isCheckCommand() || isRunCommand();
    	}
    	
    	public boolean isCheckCommand() {
    		return type==CHECK_TYPE;
    	}
    	
    	public boolean isRunCommand() {
    		return type==RUN_TYPE;
    	}
    	
    	public boolean hasExpects() {
    		return hasExpects;
    	}
    	
    	public int expectsCount() {
    		return expectsCount;
    	}
    	
    	public String toString() {
    		return toString;
    	}

		protected void setExpects(final boolean hasExpects, final int expectsCount) {
			this.hasExpects = hasExpects;
			this.expectsCount = expectsCount;
		}
    }
    
    private final Info info;

    public Info info() {
    	info.toString = toString();
		return info;
	}

    
    
    /**
     * a map from {@link alloy.ast.LeafId leaf ids} to {@link Integer} scopes.
     * the map will contain a scope for all leaf ids representing arity-1
     * relations of basic types.  it may also contain scopes for non-basic
     * types, eg. subscopes for disjoint sub-signatures.
     */
    public Map /* from LeafId to Integer */ leafId2Scope = null; 

    /**
       a mapping from {@link String} type strings to
       {@link alloy.type.SigType}s for this.  we need
       a unique mapping for each command since different
       dummy types are generated for each command
    */
    public Map stringToType = null;
    
    /**
     * a mapping from {@link LeafId}s to {@link MultiplicityExpr}s
     * for this command
     */
    public Map leafIdToMult = null;
     
    /**
     * int width for this command
     */
    public int intWidth = -1; // default value

    /** SetLeafIdsVisitor used to set leaf IDs for this command */
    public alloy.transform.SetLeafIdsVisitor sliv = null;

    /** Skolem map */
    public alloy.transform.LeafIdMap skolemMap = null;

    /** Map from LeafId to LeafId, where keys represent LeafIds of LeafExprs replaced
     * during equality reasoning and values represent the expressions that replace
     * the keys */
    public Map equivalenceMapping = null;

    /** Map from LeafId to LeafExpr, where keys represent LeafIds of LeafExprs replaced
     * during equality reasoning and values represent LeafExprs themselves */
    public Map replacedLeavesMapping = null;

    /**
     * Information about product signatures for this command.
     * Map from product signature {@link alloy.ast.LeafId leaf ids} to
     * Maps from {@link alloy.ast.LeafId leaf ids} of relations declared
     * <em>in</em> the product signature to their multiplicities, represented
     * by {@link MultiplicityExpr}s.
     */
    public Map productSigIdsToRels; // Map[LeafId -> Map[LeafId -> MultiplicityExpr] ]

    /**
     * Information about signatures which can have a scope set for this
     */
    public alloy.subscope.ScopedSigsInfo scopedSigsInfo;
    
    
    /**
     * The Module this Command belongs to.
     */
    public ModuleInfo moduleInfo;

    
	public Command(final String name_, Location location_, Scope scope_) {
        super(location_, scope_);
        this.info = new Info(name_, this);
    }


    public Command(final String name_, Scope scope_) {
        this(name_, Location.UNKNOWN, scope_);
    }



    //GET AND SET METHODS

    /**
     * gets the scope of this
     * @return the {@link Scope}
     */
    public Scope getScope() {
        return (Scope)childAt(SCOPE_INDEX);
    }

    /** set the Scope of this */
    public void setScope(Scope newChild_) {
        setChild(SCOPE_INDEX, newChild_);
    }

    /**
     * accept an AST visitor
     * @param visitor_ the visitor
     */
    protected void acceptVisitor(ASTVisitor visitor_) {
        visitor_.visit(this);
    }

    /**
     * accept a returning AST visitor
     * @param visitor_ the visitor
     * @return the Object returned by the visitor
     */
    protected Object acceptReturnVisitor(ASTReturnVisitor visitor_) {
        return visitor_.visit(this);
    }

    public String toString()
    {
        return nodeString();
    }

    public abstract FormulaPara getFormulaPara(ModuleInfo moduleInfo_);
}























